\begin{tabbing} $\forall$\=${\it es}$:ES, ${\it Cmd}$:Type, ${\it isupdate}$:(${\it Cmd}$$\rightarrow\mathbb{B}$), ${\it In}$:AbsInterface(${\it Cmd}$), ${\it Out}$:AbsInterface(Top),\+ \\[0ex]${\it expl}$:(E(${\it Out}$)$\rightarrow$(E(${\it In}$) List)). \-\\[0ex]consistent{-}updates(${\it es}$;${\it In}$;${\it Out}$;${\it Cmd}$;${\it isupdate}$;${\it expl}$) $\in$ $\mathbb{P}$ \end{tabbing}